COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Here is a suggestion for the initial paragraphs of the appendix:
C00005 ENDMK
C⊗;
Here is a suggestion for the initial paragraphs of the appendix:

Examples of Computer-checked proofs

	In chapter 3 we showed how to prove that certain recursive
LISP programs meet their specifications.  The techniques presented
in that chapter require further development before they can be
economically applied to large programs.  One requirement is that the
proofs be checked by computer, since there is just as much opportunity
for wishful thinking in writing or reading a proof of correctness as
there is in writing the program in the first place.

	This appendix contains proofs of the correctness of
%2samefringe%1 in a form acceptable to a first order logic
proof-checker called FOL developed at the Stanford University Artificial
Intelligence Laboratory.  An FOL proof is organized into several
parts.  The object of this organization is first to establish the
language in which the proof is made, then to present the general
axioms of the field of reasoning (LISP programs in the present case),
then to present the facts about the particular problem (the function
definitions in present case), and finally to give the proof itself.
If the stage has been properly set, the proof itself will be short
and comprehensible as well as acceptable to the computer.